data asm specification 
   mtd_asm

   using mtd-base

   

   
   
   
   
   procedures mtd_asm_erase# nat : pebs : error  nondeterministic;
              mtd_asm_read# nat × nat × nat × nat × pebs : buffer : bool × error  nondeterministic;
              mtd_asm_write# nat × nat × nat × nat × buffer : pebs : error  nondeterministic;
              mtd_asm_isbad# nat × pebs :  : bool × error  nondeterministic;
              mtd_asm_markbad# nat : pebs : error  nondeterministic;
              mtd_asm_get_blockcount# pebs :  : nat  ;
              mtd_asm_get_page_size# pebs :  : nat  ;
              mtd_asm_get_peb_size# pebs :  : nat  ;
              mtd_asm_init#  :  : pebs × error  nondeterministic;
   variables  PEBS : pebs flexible;
              PEB : peb flexible;
              ERR : error flexible;
              ERR0 : error flexible;
              PNUM : nat flexible;
              PNUM0 : nat flexible;
              OFFSET : nat flexible;
              BUF : buffer flexible;
              BUF0 : buffer flexible;
              N : nat flexible;
              N0 : nat flexible;
              N1 : nat flexible;
              ISBAD : bool flexible;
              isbad : bool;
              BITFLIPS : bool flexible;
              bitflips : bool;
   
   

   

   state variables  PEBS : pebs flexible;

   initialization procedure mtd_asm_init#

   if ERR = ESUCCESS

   sequential

   invariants cons :  ⊦ mtd-cons(PEBS);

   crash predicate PEBS = PEBS`

   with crash-neutrality

   

   

   

   declarations erase:
                mtd_asm_erase#(PNUM; PEBS; ERR)
                  precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad;
                  postcondition true;
                {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad
                 then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PEBS[PNUM] := mkpeb(emptypeb, 0, PEBS[PNUM].bad)}
                 else abort
                }
                read:
                mtd_asm_read#(PNUM, OFFSET, N0, N, PEBS; BUF; BITFLIPS, ERR)
                  precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF;
                  postcondition true;
                {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF
                 then {fail_or_success#(; ; ERR); BITFLIPS := ?; 
                       if ERR = ESUCCESS
                       then BUF := copy(PEBS[PNUM].data, OFFSET, BUF, N0, N)
                       else choose BUF0
                            with # BUF0 = # BUF ∧ range=(BUF0, 0, BUF, 0, N0) ∧ range=(BUF0, N0 + N, BUF, N0 + N, # BUF - N0 + N)
                            in BUF := BUF0}
                 else abort
                }
                write:
                mtd_asm_write#(PNUM, OFFSET, N0, N, BUF; PEBS; ERR)
                  precondition   PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill ≤ OFFSET ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF
                               ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE)
                ;
                  postcondition true;
                {if   PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill ≤ OFFSET ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF
                    ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE)
                 then {fail_or_success#(; ; ERR); 
                       if ERR = ESUCCESS
                       then {PEBS[PNUM].data := copy(BUF, N0, PEBS[PNUM].data, OFFSET, N); PEBS[PNUM].fill := OFFSET + N}
                       else choose N1
                            with (N1 < N ∨ N1 = 0 ∧ N = 0) ∧ is-aligned(N1, EB_PAGE_SIZE)
                            in if N1 ≠ 0 then {PEBS[PNUM].data := copy(BUF, N0, PEBS[PNUM].data, OFFSET, N1); PEBS[PNUM].fill := OFFSET + N1}}
                 else abort
                }
                isbad:
                mtd_asm_isbad#(PNUM, PEBS; ; ISBAD, ERR)
                  precondition PNUM < # PEBS;
                  postcondition true;
                {if PNUM < # PEBS
                 then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ISBAD := PEBS[PNUM].bad else ISBAD := ?}
                 else abort
                }
                markbad:
                mtd_asm_markbad#(PNUM; PEBS; ERR)
                  precondition PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad;
                  postcondition true;
                {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad
                 then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PEBS[PNUM].bad := true}
                 else abort
                }
                blockcount:mtd_asm_get_blockcount#(PEBS; ; N)  precondition true;  postcondition true;{N := # PEBS}
                page-size:mtd_asm_get_page_size#(PEBS; ; N)  precondition true;  postcondition true;{N := EB_PAGE_SIZE}
                peb-size:mtd_asm_get_peb_size#(PEBS; ; N)  precondition true;  postcondition true;{N := PEB_SIZE}
                init:
                mtd_asm_init#(; ; PEBS, ERR)
                  precondition true;
                  postcondition ERR = ESUCCESS ∨ ⌊ERR⌋ ;
                {{fail_or_success#(; ; ERR); choose pebs with ERR = ESUCCESS → mtd-cons(pebs) in PEBS := pebs}
                }
end data asm specification